Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

... Bildung.

Das heißt, wir können insbesondere alle Abraummodelle eines Programms hier nehmen,

ihren Durchschnitt bilden und damit ein weiteres Abraummodell des Programms erhalten,

das dann notwendigerweise das kleinste Abraummodell ist.

Wir hatten festgestellt, dass die Existenz so eines kleinsten Abraummodells an dem konkreten Format hängt,

dass wir für definierte Programme annehmen, insbesondere an der Tatsache,

dass es immer pro Klausel nur ein positives Literal gibt.

Wir haben uns angeschaut, ein Gegenbeispiel einer Klausel mit zwei positiven Literalen,

so etwas ganz Harmloses der Form P, A oder Q, A.

Wenn man sich so eine Klausel hernimmt, dann hat die offensichtlich kein kleinstes Abraummodell,

denn ich kann mir aussuchen, entweder P von A wahrzumachen oder Q von A wahrzumachen, jeweils sonst nichts.

Dann habe ich zwei minimale Abraummodelle, die aber untereinander unvergleichbar sind,

insbesondere gibt es also kein kleinstes.

Diese Einsicht, dass es ein kleinstes Abraummodell gibt,

befähigt uns gleichzeitig noch eine alternative Beschreibung dieses Abraummodells zu liefern.

Ich sage, das ist also der große Durchschnitt aller Abraummodelle des Programms.

Das ist ja noch kein so ganz greifbares Objekt.

Ein Korollar, was wir hier haben, ist das Folgende.

Das kleinste Abraummodell von P, das hatten wir deutsch MP genannt,

ist, wenn ich es formuliere als Teilmenge der Abraumbasis,

die Menge derjenigen Ground Atoms,

sodass gilt, P hat als logische Konsequenz eben dieses Ground Atom Phi.

Das ist ja nun eine relativ knackige Definition.

Ich mache alle Ground Atoms wahr, die ich wahrmachen muss,

und erhalte dann ein Abraummodell.

Der Beweis dafür ist nicht schwer, deswegen nenne ich es auch ein Korollar.

Die eine Richtung ist trivial, und zwar ist diese Inklusion hier.

Das ist also eine Gleichheit von zwei Mengen, die wir hier letztlich behaupten.

Das heißt, wir haben zwei Inklusionen zu zeigen.

Die Inklusion von links nach rechts, die ist deswegen klar,

weil wir eben schon festgestellt hatten, dass das hier ein Modell von P ist.

Dieses hier besagt ja gerade, jedes Modell von P erfüllt Phi.

Das heißt, da mP ein Modell von P ist, muss es also alle diese Phi hier erfüllen,

mit anderen Worten, wir haben diese Inklusion hier.

Das ist also klar, da mP tatsächlich ein Modell von P ist.

Der eigentliche Knackpunkt ist also die umgekehrte Inklusion.

Diese hier.

Da hatte ich mir einen besonders knackigen Satz draufgeschrieben.

Jetzt hatte ich hier die Reihenfolge meiner Sätze und Korollare vertauscht.

Das hier ist ein Korolar zu dem Satz, der jetzt erst folgt.

Deswegen sehe ich auch nicht mal einen Beweis, also wir machen erst den Satz.

Wie sich das bei Satz und Korolar gehört.

Das Korolar lassen wir für gleich noch stehen, beweisen erst den Satz, zu dem es ein Korolar ist.

Das ist dieser hier.

Der Satz, zu dem es ein Korolar ist, das ist der, der nun endlich enthüllt,

warum wir diese ganze Konstruktion eigentlich machen.

Und zwar hatten wir das uns auch von Anfang auf die Fahnen geschrieben,

das wird jetzt endlich erfüllt.

Wir haben hier mit dem kleinsten Abrahm-Modell ein Modell in der Hand,